A:Type, L:(A List), f1,f2:(A). (f1 = f2)  sqequal(filter(f1; L); filter(f2; L)) 

latex

Definitions	T, True, b, P  Q, P  Q, P  Q, ff, tt, if b then t else f fi , prop{i:l}, t  T, Y, reduce(f; k; as), filter(P; l), P  Q, x:A. B(x), sq_type(T), False, A, guard(T), Unit, ,
Lemmas	not assert elim, bool sq, assert elim, true wf, squash wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, eqtt to assert, bool wf